It is of enormous significance for complex technical systems or installations to be able to make statements about the dependability of the respective system or, respectively, of the installation.
It is known that statements about the dependability of an arbitrary technical system or, respectively, of an installation can be produced manually, for example by what is referred to as an error tree analysis (see DIN 25424, Part 1: Fehlerbaumanalyse: Methode und Bildzeichen; Part 2: Handrechenverfahren zur Auswertung eines Fehlerebaums) or simulatively or, respectively, analytically on the basis of models specifically produced for this purpose (see J. Dekleer and B. C. Williams, Diagnosing Multiple Faults, Elsevier Science Publishers, Artificial Intelligence, Vol. 32, 1987, pp. 97-130). For the sake of a simple presentation, only technical systems shall be mentioned below. However, technical installations are also covered in the term of technical system within the scope of this document. A complete manual determination of the influences of a technical malfunction of sensors and/or actuators is practically not possible in a complex technical system due to the linked dependencies and the different forms of realizing the control, the control system and the sensor mechanisms and/or actuator mechanisms. The analytical techniques disclosed in the Dekleer et al. reference require the production of a specific model, for which it can generally not be guaranteed that it correctly describes the system respectively under consideration. Of course, the quality of the statements is there substantially reduced. Further, a considerable disadvantage of the approaches disclosed in the Dekleer et al. reference is that the production of the model requires additional developing outlay and time. As a result thereof, a short-term investigation of alternative realizations of a technical system, which is also referred to as rapid prototyping, is prevented.
It is known to describe a technical system in a status-finite description, for example as automat. A status-finite description usually comprises statuses in which actions are implemented when the technical system is in the respective status. Further, the status-finite description usually comprises status transitions that describe possible changes of the technical system between statuses. The technical system can also implement actions in status transitions. It is known in this context in a controlled, technical system to fashion the status-finite description such that the behavior of the control of the technical system and the behavior of the controlled installation is presented as status automat. It is also not assured given these approaches that all possible influences of errors on the system are correctly identified.
Possibilities for textual description of a status automat that are processed with a computer are, for example, interlocking specification language (ISL) or control specification language (CSL), which are described in K. Nökel, K. Winkelmann, Controller Synthesis and Verification: A Case Study, in: C. Leverentz, T. Lindner, Formal Development of Reactive Systems, Lecture Notes in Computer Science (No. 891), Springer 1995, pp. 55-74.
It is also known to employ a status-finite description for generating controls with a computer and for the computer-supported documentation of properties of an error-free technical system.
One possibility for computer-supported documentation of properties of an error-free technical system employs the principle of what is referred to as model checking, this being described in J. Burch et al, Symbolic Model Checking for Sequential Circuit Verification, IEEE Trans. On Computer-Aided Design of Integrated Circuits and Systems, Vol. 13, No. 4, pp. 401-424, April 1994.
It is also known for status-finite description of a system to employ what is referred to as a finite state machine format (FSM Format) whose fundamentals are described in R. Bryant, Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams, ACM Computing Survey, Vol. 24, No. 3, pp. 293-318, September 1992. Binary decision diagrams (BDD) have the advantage of also compactly representing very extensive status systems in many instances.